(DECLARE (*FEXPR THAPPLY THGENAME THSTATE THANTE THERASING THCONSE THDUMP
		 THRESTRICT THBKPT THUNIQUE)
	 (*FEXPR THVSETQ THMESSAGE THDO THGOAL THERASE THAND THNV THSUCCEED
		 THAMONG THCOND THSETQ)
	 (*FEXPR THASSERT THASVAL THERT THGO THFAIL THOR THFIND THFINALIZE
		 THRETURN THPROG THFLUSH)
	 (*FEXPR THNOT THV THTRACE THGENS)
	 (*LSUBR THMATCH)
	 (SPECIAL THLAS OBLIST THINF THGENAME THGENS THZ THY THX THALIST
		  THABRANCH THBRANCH)
	 (SPECIAL THV /0RETVAL /0LISTEN THL /0RETFLAG THE /0LEVEL THXX THTT TYPE
		  THWH THON THML)
	 (SPECIAL THBS THNF THPC XX THAL THZ1 THY1 ↑A THTTL THA2 LASTWORD THFSTP
		  THFST)
	 (SPECIAL THUSERCHARS THEXP THTREE THLEVEL THTRACE THPRD THMESSAGE
		  THUSERMESSAGES)
	 (SPECIAL THUNREADFLG THUNREAD1 THUNREAD2 THOLIST THVALUE THUSERINITFN)
	 (SPECIAL BASE *NOPOINT %%TIME %%DTIME %%GCTIME %%SPEAK)
         (*SUBR THBRANCH)
	 (DE THCMPDEF 
	     (X)
	     (COND [(ATOM (CADDR X)) (FLUSHEXPR X)]
		   [T (COMPFUNC (CADR X) (CONS @SUBR (CDADDR X)) (CADDDR X))]))
	 (DEFLIST (THFAIL THSUCCEED THTRACE) THCMPDEF DEFACTION))

(DEFPROP THPUSH
 (LAMBDA (A)
  (LIST @SETQ (CADR A) (LIST @CONS (CADDR A) (CADR A))))
 MACRO)

(DEFPROP THPOPT
 (LAMBDA (L) @(SETQ THTREE (CDR THTREE)))
 MACRO)

(DEFPROP EVLIS
 (LAMBDA (X) (MAPC (FUNCTION EVAL) X))
 EXPR)

(DEFPROP THPRINT2
 (LAMBDA (X) (PRINC @/ ) (PRINC X))
 EXPR)

(DEFPROP THPRINTC
 (LAMBDA (X) (TERPRI) (PRINC X) (PRINC @/ ))
 EXPR)

(DEFPROP THADD
 (LAMBDA (THTT THPL)
  (PROG (THNF THWH THCK THLAS THTTL THT1 THFST THFSTP THFOO)
	(SETQ THCK 
	      (COND [(ATOM THTT)
		     (OR [SETQ THT1 (GET THTT @THEOREM)]
			 [PROG2 (PRINT THTT)
				(THERT CANT THASSERT/, NO THEOREM - THADD)])
		     (SETQ THWH (CAR THT1))
		     (SETQ THTTL THTT)
		     (AND THPL 
			  [PROG NIL
			     LP (THPUTPROP THTT (CADR THPL) (CAR THPL))
				(COND [(SETQ THPL (CDDR THPL)) (GO LP)])])
		     (CADDR THT1)]
		    [T (SETQ THWH @THASSERTION)
		       (SETQ THTTL (CONS THTT THPL))
		       THTT]))
	(SETQ THNF 0Q)
	(SETQ THLAS (LENGTH THCK))
	(SETQ THFST T)
   THP1 (COND [(NULL THCK)
	       (SETQ THCK THFOO)
	       (SETQ THNF 0Q)
	       (SETQ THFOO (SETQ THFST NIL))
	       (SETQ THFSTP T)
	       (GO THP1)]
	      [(NULL (SETQ THT1 (THIP (CAR THCK)))) (RETURN NIL)]
	      [(EQ THT1 @THOK)]
	      [(SETQ THFOO 
		     (NCONC THFOO (LIST (COND [(EQ THT1 @THVRB) (CAR THCK)]))))
	       (SETQ THCK (CDR THCK))
	       (GO THP1)])
	(SETQ THFST NIL)
	(MAPC (FUNCTION THIP) (CDR THCK))
	(SETQ THNF 0Q)
	(MAPC (FUNCTION THIP) THFOO)
	(RETURN THTTL)))
 EXPR)

(DEFPROP THAMONG
 (LAMBDA (THA)
  (COND [(EQ (CADR (SETQ THXX 
			 (THGAL (COND [(EQ (CAAR THA) @THEV)
				       (THVAL (CADAR THA) THALIST)]
				      [T (CAR THA)])
				THALIST)))
	     @THUNASSIGNED)
	 (THPUSH THTREE (LIST @THAMONG THXX (THVAL (CADR THA) THALIST)))
	 NIL]
	[T (MEMBER (CADR THXX) (THVAL (CADR THA) THALIST))]))
 FEXPR)

(DEFPROP THAMONG THAMONGF THFAIL)

(DEFPROP THAMONGF
 (LAMBDA NIL
  (COND [THMESSAGE (THPOPT) NIL]
	[(CADDAR THTREE)
	 (RPLACA (CDADAR THTREE) (CAADDR (CAR THTREE)))
	 (RPLACA (CDDAR THTREE) (CDADDR (CAR THTREE)))
	 (SETQ THBRANCH THTREE)
	 (SETQ THABRANCH THALIST)
	 (THPOPT)
	 T]
	[T (RPLACA (CDADAR THTREE) @THUNASSIGNED) (THPOPT) NIL]))
 EXPR)

(DEFPROP THAND
 (LAMBDA (A)
  (OR [NOT A] [PROG2 (THPUSH THTREE (LIST @THAND A NIL)) (SETQ THEXP (CAR A))]))
 FEXPR)

(DEFPROP THAND THANDT THSUCCEED)

(DEFPROP THAND THANDF THFAIL)

(DEFPROP THANDF
 (LAMBDA NIL (THBRANCHUN) NIL)
 EXPR)

(DEFPROP THANDT
 (LAMBDA NIL
  (COND [(CDADAR THTREE)
	 (THBRANCH)
	 (SETQ THEXP (CADR (CADAR THTREE)))
	 (RPLACA (CDAR THTREE) (CDADAR THTREE))]
	[(THPOPT)])
  THVALUE)
 EXPR)

(DEFPROP THANTE
 (LAMBDA (THX) (THDEF @THANTE THX))
 FEXPR)

(DEFPROP THAPPLY
 (LAMBDA (L)
  (THAPPLY1 (CAR L) (GET (CAR L) @THEOREM) (CADR L)))
 FEXPR)

(DEFPROP THAPPLY1
 (LAMBDA (THM THB DAT)
  (COND [(AND [THBIND (CADR THB)] [THMATCH1 DAT (CADDR THB)])
	 (AND THTRACE [THTRACES @THEOREM THM])
	 (THPUSH THTREE @(THEOREM))
	 (THPUSH THTREE (LIST @THPROG (CDDR THB) NIL (CDDR THB)))
	 (THPROGA)
	 T]
	[T (SETQ THALIST THOLIST) (THPOPT) NIL]))
 EXPR)

(DEFPROP THEOREM THPOPTV THSUCCEED)

(DEFPROP THEOREM THPOPTV THFAIL)

(DEFPROP THEOREM
 (LAMBDA (X B)
  (THPUSH THTREE 
	  (LIST @THTRACES X @(AND THVALUE [PRIN1 THVALUE]) (AND B @[THERT])))
  (THPRINTC @ENTERING/ THEOREM)
  (PRIN1 X))
 THTRACE)

(DEFPROP THASS1
 (LAMBDA (THA P)
  (PROG (THX THY1 THY TYPE PSEUDO)
	(AND [CDR THA] [EQ (CAADR THA) @THPSEUDO] [SETQ PSEUDO T])
	(OR [ATOM (SETQ THX (CAR THA))]
	    [THPURE (SETQ THX (THVARSUBST THX NIL))]
	    PSEUDO 
	    [PROG2 (PRINT THX) (THERT IMPURE ASSERTION OR ERASURE - THASS1)])
	(AND THTRACE 
	     [NOT PSEUDO]
	     [THTRACES (COND [P @THASSERT] [@THERASE]) THX])
	(SETQ THA (COND [PSEUDO (CDDR THA)] [(CDR THA)]))
	(COND
	 [(SETQ THX 
		(COND [PSEUDO (LIST THX)]
		      [P (THADD THX 
				(SETQ THY 
				      (COND [(AND THA [EQ (CAAR THA) @THPROP])
					     (PROG1 (EVAL (CADAR THA))
						    (SETQ THA (CDR THA)))])))]
		      [T (THREMOVE THX)]))]
	 [T (RETURN NIL)])
	(COND [P (SETQ TYPE @THANTE)] [(SETQ TYPE @THERASING)])
	(OR PSEUDO 
	    [THPUSH THTREE (LIST (COND [P @THASSERT] [@THERASE]) THX THY)])
	(SETQ THY (MAPCAN (FUNCTION THTAE) THA))
	(COND [THY (SETQ THEXP (CONS @THDO THY))])
	(RETURN THX)))
 EXPR)

(DEFPROP THASSERT
 (LAMBDA (THA) (THASS1 THA T))
 FEXPR)

(DEFPROP THASSERT THASSERTT THSUCCEED)

(DEFPROP THASSERT THASSERTF THFAIL)

(DEFPROP THASSERT
 (LAMBDA (X B)
  (THPUSH THTREE (LIST @THTRACES (THGENS A) (AND B @[THERT])))
  (PRINT @ASSERTING)
  (PRIN1 (CADAR THTREE))
  (PRINC @/ )
  (PRIN1 X))
 THTRACE)

(DEFPROP THASSERTF
 (LAMBDA NIL
  (THREMOVE (COND [(ATOM (CADAR THTREE)) (CADAR THTREE)] [T (CAADAR THTREE)]))
  (THPOPT)
  NIL)
 EXPR)

(DEFPROP THASSERTT
 (LAMBDA NIL (PROG1 (CADAR THTREE) (THPOPT)))
 EXPR)

(DEFPROP THASVAL
 (LAMBDA (X)
  (AND [SETQ X (THSGAL X)] [NEQ (CADR X) @THUNASSIGNED]))
 FEXPR)

(DEFPROP THBA
 (LAMBDA (TH1 TH2)
  (PROG (THP)
	(SETQ THP TH2)
   THP1 (AND [EQ (COND [THPC (CADR THP)] [T (CAADR THP)]) TH1] [RETURN THP])
	(COND [(CDR (SETQ THP (CDR THP)))] [T (RETURN NIL)])
	(GO THP1)))
 EXPR)

(DEFPROP THBAP
 (LAMBDA (TH1 TH2)
  (PROG (THP)
	(SETQ THP TH2)
   THP1 (AND [EQUAL (COND [THPC (CADR THP)] [T (CAADR THP)]) TH1] [RETURN THP])
	(COND [(CDR (SETQ THP (CDR THP)))] [T (RETURN NIL)])
	(GO THP1)))
 EXPR)

(DEFPROP THBIND
 (LAMBDA (A)
  (SETQ THOLIST THALIST)
  (OR [NULL A]
      [PROG NIL
	 GO (COND [(NULL A)
		   (THPUSH THTREE (LIST @THREMBIND THOLIST))
		   (RETURN T)])
	    (THPUSH THALIST 
		    (COND [(ATOM (CAR A)) (LIST (CAR A) @THUNASSIGNED)]
			  [(EQ (CAAR A) @THRESTRICT)
			   (NCONC (THBI1 (CADAR A)) (CDDAR A))]
			  [T (LIST (CAAR A) (EVAL (CADAR A)))]))
	    (SETQ A (CDR A))
	    (GO GO)]))
 EXPR)

(DEFPROP THBI1
 (LAMBDA (X)
  (COND [(ATOM X) (LIST X @THUNASSIGNED)] [T (LIST (CAR X) (EVAL (CADR X)))]))
 EXPR)

(DEFPROP THBKPT
 (LAMBDA (L)
  (OR [AND THTRACE [THTRACES @THBKPT L]] THVALUE))
 FEXPR)

(DEFPROP THBKPT
 (LAMBDA (X B)
  (THPUSH THTREE (LIST @THTRACES (THGENS B) (AND B @[THERT])))
  (THPRINTC @PASSING/ BKPT)
  (PRIN1 (CADAR THTREE))
  (PRINC @/ )
  (SETQ THBRANCH THTREE)
  (SETQ THABRANCH THALIST)
  (THPOPT)
  (PRIN1 X))
 THTRACE)

(DEFPROP THBRANCH
 (LAMBDA NIL
  (COND [(NOT (CDADAR THTREE))]
	[(EQ THBRANCH THTREE) (SETQ THBRANCH NIL)]
	[(RPLACA (CDDAR THTREE)
		 (CONS (LIST THBRANCH THABRANCH (CADAR THTREE)) (CADDAR THTREE))
	  )
	 (SETQ THBRANCH NIL)]))
 EXPR)

(DEFPROP THBRANCHUN
 (LAMBDA NIL
  (PROG (X)
	(RETURN (COND [(SETQ X (CADDAR THTREE))
		       (RPLACA (CDAR THTREE) (CADDAR X))
		       (RPLACA (CDDAR THTREE) (CDR X))
		       (SETQ THALIST (CADAR X))
		       (SETQ THTREE (CAAR X))
		       T]
		      [T (THPOPT) NIL]))))
 EXPR)

(DEFPROP THCOND
 (LAMBDA (THA)
  (THPUSH THTREE (LIST @THCOND THA NIL))
  (SETQ THEXP (CAAR THA)))
 FEXPR)

(DEFPROP THCOND THCONDT THSUCCEED)

(DEFPROP THCOND THCONDF THFAIL)

(DEFPROP THCONDF (LAMBDA NIL (THOR2 NIL)) EXPR)

(DEFPROP THCONDT
 (LAMBDA NIL
  (RPLACA (CAR THTREE) @THAND)
  (RPLACA (CDAR THTREE) (CAADAR THTREE))
  THVALUE)
 EXPR)

(DEFPROP THCONSE
 (LAMBDA (THX) (THDEF @THCONSE THX))
 FEXPR)

(DEFPROP THDATA
 (LAMBDA NIL
  (PROG (X)
     GO (TERPRI)
	(COND [(NULL (SETQ X (READ))) (RETURN T)]
	      [(PRINT (THADD (CAR X) (CDR X)))])
	(GO GO)))
 EXPR)

(DEFPROP THDEF
 (LAMBDA (THMTYPE THX)
  (PROG (THNOASSERT? THMNAME THMBODY)
	(COND [(NOT (ATOM (CAR THX)))
	       (SETQ THMBODY THX)
	       (COND [(EQ THMTYPE @THCONSE) (SETQ THMNAME (THGENAME TC-G))]
		     [(EQ THMTYPE @THANTE) (SETQ THMNAME (THGENAME TA-G))]
		     [(EQ THMTYPE @THERASING) (SETQ THMNAME (THGENAME TE-G))])]
	      [(SETQ THMNAME (CAR THX)) (SETQ THMBODY (CDR THX))])
	(COND [(EQ (CAR THMBODY) @THNOASSERT)
	       (SETQ THNOASSERT? T)
	       (SETQ THMBODY (CDR THMBODY))])
	(THPUTPROP THMNAME (CONS THMTYPE THMBODY) @THEOREM)
	(COND [THNOASSERT? (PRINT (LIST THMNAME @DEFINED @BUT @NOT @ASSERTED))]
	      [(THASS1 (LIST THMNAME) T)
	       (PRINT (LIST THMNAME @DEFINED @AND @ASSERTED))]
	      [T (PRINT (LIST THMNAME @REDEFINED))])
	(RETURN T)))
 EXPR)

(DEFPROP THDO
 (LAMBDA (A)
  (OR [NOT A]
      [PROG2 (THPUSH THTREE (LIST @THDO A NIL NIL)) (SETQ THEXP (CAR A))]))
 FEXPR)

(DEFPROP THDO THDOB THSUCCEED)

(DEFPROP THDO THDOB THFAIL)

(DEFPROP THDO1
 (LAMBDA NIL
  (RPLACA (CDAR THTREE) (CDADAR THTREE))
  (SETQ THEXP (CAADAR THTREE))
  (COND [THBRANCH (RPLACA (CDDAR THTREE) (CONS THBRANCH (CADDAR THTREE)))
		  (SETQ THBRANCH NIL)
		  (RPLACA (CDDDAR THTREE)
			  (CONS THABRANCH (CAR (CDDDAR THTREE))))]))
 EXPR)

(DEFPROP THDOB
 (LAMBDA NIL
  (COND [(OR THMESSAGE [NULL (CDADAR THTREE)]) (RPLACA (CAR THTREE) @THUNDO) T]
	[(THDO1)]))
 EXPR)

(DEFPROP THDUMP
 (LAMBDA (THFILE)
  (OUTC (PROG1 (OUTC (EVAL (LIST @OUTPUT @DSK: (CAR THFILE))) NIL)
	       (EVAL (CONS @THSTATE (CDR THFILE))))
	T))
 FEXPR)

(DEFPROP THERASE
 (LAMBDA (THA) (THASS1 THA NIL))
 FEXPR)

(DEFPROP THERASE THERASET THSUCCEED)

(DEFPROP THERASE THERASEF THFAIL)

(DEFPROP THERASE
 (LAMBDA (X B)
  (THPUSH THTREE (LIST @THTRACES (THGENS E) (AND B @[THERT])))
  (PRINT @ERASING)
  (PRIN1 (CADAR THTREE))
  (PRINC @/ )
  (PRIN1 X))
 THTRACE)

(DEFPROP THERASEF
 (LAMBDA NIL
  (THADD (COND [(ATOM (CADAR THTREE)) (CADAR THTREE)] [T (CAADAR THTREE)])
	 (COND [(ATOM (CADAR THTREE)) NIL] [T (CDADAR THTREE)]))
  (THPOPT)
  NIL)
 EXPR)

(DEFPROP THERASET
 (LAMBDA NIL (PROG1 (CADAR THTREE) (THPOPT)))
 EXPR)

(DEFPROP THERASING
 (LAMBDA (THX) (THDEF @THERASING THX))
 FEXPR)

(DEFPROP THFAIL
 (LAMBDA (THA)
  (AND THA 
       [PROG (THTREE1 THA1 THX)
	   F (COND [(EQ (CAR THA) @THTAG) (SETQ THA1 @THPROG)]
		   [(EQ (CAR THA) @THINF) (SETQ THINF T) (RETURN NIL)]
		   [(EQ (CAR THA) @THMESSAGE)
		    (SETQ THMESSAGE (CADR THA))
		    (RETURN NIL)]
		   [T (SETQ THA1 (CAR THA))])
	     (SETQ THTREE1 THTREE)
	 LP1 (COND [(NULL THTREE1)
		    (PRINT THA)
		    (COND [(ATOM (SETQ THA (THERT NOT FOUND - THFAIL)))
			   (RETURN THA)]
			  [T (GO F)])]
		   [(EQ (CAAR THTREE1) THA1) (GO ELP1)])
	ALP1 (SETQ THTREE1 (CDR THTREE1))
	     (GO LP1)
	ELP1 (COND [(EQ (CAR THA) @THTAG)
		    (COND [(MEMQ (CADR THA) (CADDDR (CAR THTREE1))) (GO TAGS)]
			  [T (GO ALP1)])])
	     (SETQ THMESSAGE (LIST (CDR THTREE1) (AND [CDR THA] [CADR THA])))
	     (RETURN NIL)
	TAGS (SETQ THX (CADDAR THTREE1))
	 LP2 (COND [(NULL THX) (GO ALP1)]
		   [(EQ (CAADDR (CAR THX)) (CADR THA))
		    (SETQ THMESSAGE 
			  (LIST (CAAR THX) (AND [CDDR THA] [CADDR THA])))
		    (RETURN NIL)])
	     (SETQ THX (CDR THX))
	     (GO LP2)]))
 FEXPR)

(DEFPROP THFAIL?
 (LAMBDA (PRD ACT)
  (THPUSH THTREE (LIST @THFAIL? PRD ACT))
  THVALUE)
 EXPR)

(DEFPROP THFAIL? THPOPTV THSUCCEED)

(DEFPROP THFAIL? THFAIL?F THFAIL)

(DEFPROP THFAIL?F
 (LAMBDA NIL
  (COND [(EVAL (CADAR THTREE))
	 (PROG2 (SETQ THMESSAGE NIL) (EVAL (CADDAR THTREE)) (THPOPT))]
	[T (THPOPT) NIL]))
 EXPR)

(DEFPROP THFINALIZE
 (LAMBDA (THA)
  (PROG (THTREE1 THT THX)
	(COND [(NULL THA) (SETQ THA (THERT BAD CALL - THFINALIZE))])
	(COND [(ATOM THA) (RETURN THA)]
	      [(EQ (CAR THA) @THTAG) (SETQ THT (CADR THA))])
	(SETQ THTREE (SETQ THTREE1 (CONS NIL THTREE)))
   PLUP (SETQ THX (CADR THTREE1))
	(COND [(NULL (CDR THTREE1)) (PRINT THA) (THERT OVERPOP - THFINALIZE)]
	      [(AND THT [EQ (CAR THX) @THPROG] [MEMQ THT (CADDDR THX)])
	       (GO RTLEV)]
	      [(OR [EQ (CAR THX) @THPROG] [EQ (CAR THX) @THAND])
	       (RPLACA (CDDR THX) NIL)
	       (SETQ THTREE1 (CDR THTREE1))]
	      [(EQ (CAR THX) @THREMBIND) (SETQ THTREE1 (CDR THTREE1))]
	      [(RPLACD THTREE1 (CDDR THTREE1))])
	(COND [(EQ (CAR THX) (CAR THA)) (GO DONE)])
	(GO PLUP)
  RTLEV (SETQ THX (CDDR THX))
  LEVLP (COND [(NULL (CAR THX)) (SETQ THTREE1 (CDR THTREE1)) (GO PLUP)]
	      [(EQ (CAADDR (CAAR THX)) THT) (GO DONE)])
	(RPLACA THX (CDAR THX))
	(GO LEVLP)
   DONE (THPOPT)
	(RETURN T)))
 FEXPR)

(DEFPROP THFIND
 (LAMBDA (THA)
  (THBIND (CADDR THA))
  (THPUSH THTREE 
	  (LIST @THFIND
		(COND [(EQ (CAR THA) @ALL) @(1Q NIL NIL)]
		      [(NUMBERP (CAR THA)) (LIST (CAR THA) (CAR THA) T)]
		      [(NUMBERP (CAAR THA)) (CAR THA)]
		      [(EQ (CAAR THA) @EXACTLY)
		       (LIST (CADAR THA) (ADD1 (CADAR THA)) NIL)]
		      [(EQ (CAAR THA) @AT-MOST)
		       (LIST 1Q (ADD1 (CADAR THA)) NIL)]
		      [(EQ (CAAR THA) @AS-MANY-AS) (LIST 1Q (CADAR THA) T)]
		      [T (CONS (CADAR THA)
			       (COND [(NULL (CDDAR THA)) (LIST NIL T)]
				     [(EQ (CADDAR THA) @AT-MOST)
				      (LIST (ADD1 (CAR (CDDDAR THA))) NIL)]
				     [T (LIST (CAR (CDDDAR THA)) T)]))])
		(CONS 0Q NIL)
		(CADR THA)))
  (THPUSH THTREE (LIST @THPROG (CDDR THA) NIL (CDDR THA)))
  (THPROGA))
 FEXPR)

(DEFPROP THFIND THFINDT THSUCCEED)

(DEFPROP THFIND THFINDF THFAIL)

(DEFPROP THFINDF
 (LAMBDA NIL
  (SETQ THBRANCH NIL)
  (COND [(OR THMESSAGE [LESSP (CAADR (SETQ THXX (CDAR THTREE))) (CAAR THXX)])
	 (THPOPT)
	 NIL]
	[T (THPOPT) (CDADR THXX)]))
 EXPR)

(DEFPROP THFINDT
 (LAMBDA NIL
  (PROG (THX THY THZ THCDAR)
	(SETQ THZ (CADDR (SETQ THCDAR (CDAR THTREE))))
	(AND [MEMBER (SETQ THX (THVARSUBST THZ NIL)) (CDADR THCDAR)] [GO GO])
	(RPLACD (CADR THCDAR) (CONS THX (CDADR THCDAR)))
	(COND [(EQ (SETQ THY (ADD1 (CAADR THCDAR))) (CADAR THCDAR))
	       (RETURN (PROG2 (SETQ THBRANCH NIL)
			      (AND [CADDAR THCDAR] [CDADR THCDAR])
			      (THPOPT)))])
	(RPLACA (CADR THCDAR) THY)
     GO (SETQ THTREE THBRANCH)
	(SETQ THALIST THABRANCH)
	(SETQ THBRANCH NIL)
	(RETURN NIL)))
 EXPR)

(DEFPROP THFLUSH
 (LAMBDA (A)
  (MAPC (FUNCTION (LAMBDA (B)
		   (MAPC (FUNCTION (LAMBDA (C)
				    (MAPC (FUNCTION (LAMBDA (D) (REMPROP D B)))
					  C)))
			 OBLIST)))
	(SETQ A (OR A @[THASSERTION THCONSE THANTE THERASING])))
  A)
 FEXPR)

(DEFPROP THGAL
 (LAMBDA (X Y)
  (SETQ THXX X)
  (OR [ASSOC (CADR X) Y] [PROG2 (PRINT THXX) (THERT THUNBOUND THGAL)]))
 EXPR)

(DEFPROP THGENAME
 (LAMBDA (X)
  (PROG (BASE *NOPOINT)
	(SETQ BASE 12Q)
	(SETQ *NOPOINT T)
	(RETURN (READLIST (NCONC (EXPLODE (CAR X))
				 (EXPLODE (SETQ THGENAME (ADD1 THGENAME))))))))
 FEXPR)

(DEFV THGENAME 0Q)

(DEFPROP THGO
 (LAMBDA (X)
  (APPLY# @THSUCCEED (CONS @THTAG X)))
 FEXPR)

(DEFPROP THGOAL
 (LAMBDA (THA)
  (PROG (THY THY1 THZ THZ1 THA1 THA2)
	(SETQ THA2 (THVARSUBST (CAR THA) T))
	(SETQ THA1 (CDR THA))
	(COND [(OR [NULL THA1]
		   [AND [NOT (AND [EQ (CAAR THA1) @THANUM]
				  [SETQ THA1 
					(CONS (LIST @THNUM (CADAR THA1))
					      (CONS (LIST @THDBF @THTRUE)
						    (CDR THA1)))])]
			[NOT (AND [EQ (CAAR THA1) @THNODB]
				  [PROG2 (SETQ THA1 (CDR THA1)) T])]
			[NOT (EQ (CAAR THA1) @THDBF)]])
	       (SETQ THA1 (CONS (LIST @THDBF @THTRUE) THA1))])
	(SETQ THA1 (MAPCAN (FUNCTION THTRY) THA1))
	(AND THTRACE [THTRACES @THGOAL THA2])
	(COND [(NULL THA1) (RETURN NIL)])
	(THPUSH THTREE (LIST @THGOAL THA2 THA1))
	(RPLACD (CDDAR THTREE) 777777Q)
	(RETURN NIL)))
 FEXPR)

(DEFPROP THGOAL THGOALT THSUCCEED)

(DEFPROP THGOAL THGOALF THFAIL)

(DEFPROP THGOAL
 (LAMBDA (X B)
  (THPUSH THTREE 
	  (LIST @THTRACES
		(THGENS G)
		@(AND THVALUE [PRIN1 THVALUE])
		(AND B @[THERT])))
  (THPRINTC @TRYING/ GOAL)
  (PRIN1 (CADAR THTREE))
  (PRINC @/ )
  (PRIN1 X))
 THTRACE)

(DEFPROP THGOALF
 (LAMBDA NIL
  (COND [THMESSAGE (THPOPT) NIL] [(THTRY1)] [T (THPOPT) NIL]))
 EXPR)

(DEFPROP THGOALT
 (LAMBDA NIL
  (PROG1 (COND [(EQ THVALUE @THNOVAL) (LIST (THVARSUBST (CADAR THTREE) NIL))]
	       [THVALUE])
	 (THPOPT)))
 EXPR)

(DEFPROP THIP
 (LAMBDA (THI)
  (PROG (THT1 THT3 THSV THT2 THI1)
	(SETQ THNF (ADD1 THNF))
	(COND [(NUMBERP THI) (RETURN @THVRB)]
	      [(AND [ATOM THI] [NOT (EQ THI @?)] [NOT (NUMBERP THI)])
	       (SETQ THI1 THI)]
	      [(OR [EQ THI @?] [MEMQ (CAR THI) @(THV THNV)])
	       (COND [THFST (RETURN @THVRB)] [(SETQ THI1 @THVRB)])]
	      [T (RETURN @THVRB)])
	(COND [(NOT (SETQ THT1 (GET THI1 THWH)))
	       (PUTPROP THI1 (LIST NIL (LIST THNF (LIST THLAS 1Q THTTL))) THWH)]
	      [(EQ THT1 @THNOHASH) (RETURN @THBQF)]
	      [(NOT (SETQ THT2 (ASSOC THNF (CDR THT1))))
	       (NCONC THT1 (LIST (LIST THNF (LIST THLAS 1Q THTTL))))]
	      [(NOT (SETQ THT3 (ASSOC THLAS (CDR THT2))))
	       (NCONC THT2 (LIST (LIST THLAS 1Q THTTL)))]
	      [(AND [OR THFST THFSTP]
		    [COND [(EQ THWH @THASSERTION) (ASSOC# THTT (CDDR THT3))]
			  [T (MEMQ THTT (CDDR THT3))]])
	       (RETURN NIL)]
	      [(SETQ THSV (CDDR THT3))
	       (RPLACA (CDR THT3) (ADD1 (CADR THT3)))
	       (RPLACD (CDR THT3) (NCONC (LIST THTTL) THSV))])
	(RETURN @THOK)))
 EXPR)

(DEFPROP THMATCH2
 (LAMBDA (THX THY)
  (AND [CONSP THX] [EQ (CAR THX) @THEV] [SETQ THX (THVAL (CADR THX) THOLIST)])
  (AND [CONSP THY] [EQ (CAR THY) @THEV] [SETQ THY (THVAL (CADR THY) THALIST)])
  (COND [(EQ THX @?)]
	[(EQ THY @?)]
	[(OR [AND [CONSP THX] [MEMQ (CAR THX) @(THV THNV THRESTRICT)]]
	     [AND [CONSP THY] [MEMQ (CAR THY) @(THV THNV THRESTRICT)]])
	 ((LAMBDA (XPAIR YPAIR)
	   (COND [(AND XPAIR 
		       [OR [EQ (CAR THX) @THNV]
			   [AND [EQ (CAR THX) @THV]
				[EQ (CADR XPAIR) @THUNASSIGNED]]]
		       [THCHECK (CDDR XPAIR)
				(COND [YPAIR (CADR YPAIR)] [T THY])])
		  (COND [YPAIR (THRPLACAS (CDR XPAIR) (CADR YPAIR))
			       (AND [CDDR YPAIR]
				    [THRPLACDS (CDR XPAIR)
					       (THUNION (CDDR XPAIR)
							(CDDR YPAIR))])
			       (THRPLACDS YPAIR (CDR XPAIR))]
			[T (THRPLACAS (CDR XPAIR) THY)])]
		 [(AND YPAIR 
		       [OR [EQ (CAR THY) @THNV]
			   [AND [EQ (CAR THY) @THV]
				[EQ (CADR YPAIR) @THUNASSIGNED]]]
		       [THCHECK (CDDR YPAIR)
				(COND [XPAIR (CADR XPAIR)] [T THX])])
		  (COND [XPAIR (THRPLACAS (CDR YPAIR) (CADR XPAIR))]
			[T (THRPLACAS (CDR YPAIR) THX)])]
		 [(AND XPAIR 
		       [EQUAL (CADR XPAIR) (COND [YPAIR (CADR YPAIR)] [T THY])])
		  ]
		 [(AND YPAIR [EQUAL (CADR YPAIR) THX])]
		 [T (ERR NIL)]))
	  (COND [(THVAR THX) (THGAL THX THOLIST)]
		[(AND [CONSP THX] [EQ (CAR THX) @THRESTRICT])
		 (COND [(EQ (CADR THX) @?)
			(PROG1 (CONS @?
				     (CONS @THUNASSIGNED
					   (APPEND (CDDR THX) NIL)))
			       (SETQ THX @(THNV ?)))]
		       [T ((LAMBDA (U)
			    (THRPLACDS (CDR U) (THUNION (CDDR U) (CDDR THX)))
			    (SETQ THX (CADR THX))
			    U)
			   (THGAL (CADR THX) THOLIST))])])
	  (COND [(THVAR THY) (THGAL THY THALIST)]
		[(AND [CONSP THY] [EQ (CAR THY) @THRESTRICT])
		 (COND [(EQ (CADR THY) @?)
			(PROG1 (CONS @?
				     (CONS @THUNASSIGNED
					   (APPEND (CDDR THY) NIL)))
			       (SETQ THY @(THNV ?)))]
		       [T ((LAMBDA (U)
			    (THRPLACDS (CDR U) (THUNION (CDDR U) (CDDR THY)))
			    (SETQ THY (CADR THY))
			    U)
			   (THGAL (CADR THY) THALIST))])]))]
	[(EQUAL THX THY)]
	[T (ERR NIL)]))
 EXPR)

(DEFPROP THCHECK
 (LAMBDA (THPRD THX)
  (OR [NULL THPRD]
      [EQ THX @THUNASSIGNED]
      [ERRSET (MAPC (FUNCTION (LAMBDA (THY) (OR [THY THX] [ERR NIL]))) THPRD)]))
 EXPR)

(DEFPROP THUNION
 (LAMBDA (L1 L2)
  (MAPC (FUNCTION (LAMBDA (THX)
		   (COND [(MEMBER THX L2)] [T (SETQ L2 (CONS THX L2))])))
	L1)
  L2)
 EXPR)

(DEFPROP THMATCH
 (LAMBDA THX
  ((LAMBDA (THOLIST THALIST)
    (THMATCH1 (ARG 1Q) (ARG 2Q)))
   (COND [(GREATERP THX 2Q) (ARG 3Q)] [T THALIST])
   (COND [(GREATERP THX 3Q) (ARG 4Q)] [T THALIST])))
 EXPR)

(DEFPROP THMATCH1
 (LAMBDA (THX THY)
  (PROG (THML)
	(COND [(AND [EQ (LENGTH (COND [(EQ (CAR THX) @THEV)
				       (SETQ THX (THVAL (CADR THX) THOLIST))]
				      [THX]))
			(LENGTH THY)]
		    [ERRSET (MAPC (FUNCTION THMATCH2) THX THY)])
	       (AND THML [THPUSH THTREE (LIST @THMUNG THML)])
	       (RETURN T)]
	      [T (EVLIS THML) (RETURN NIL)])))
 EXPR)

(DEFPROP THMATCHLIST
 (LAMBDA (THTB THWH)
  (PROG (THB1 THB2 THL THNF THAL THA1 THA2 THRN THL1 THL2 THRVC)
	(SETQ THL 377777777777Q)
	(SETQ THNF 0Q)
	(SETQ THAL (LENGTH THTB))
	(SETQ THB1 THTB)
   THP1 (COND [THB1] [T (RETURN (COND [THL2 (APPEND THL1 THL2)] [THL1]))])
	(SETQ THNF (ADD1 THNF))
	(SETQ THB2 (CAR THB1))
	(SETQ THB1 (CDR THB1))
   THP3 (COND [(OR [NULL (ATOM THB2)] [NUMBERP THB2] [EQ THB2 @?]) (GO THP1)]
	      [(NOT (SETQ THA1 (GET THB2 THWH))) (SETQ THA1 @(0Q 0Q))]
	      [(EQ THA1 @THNOHASH) (GO THP1)]
	      [(NOT (SETQ THA1 (ASSOC THNF (CDR THA1)))) (SETQ THA1 @(0Q 0Q))]
	      [(NOT (SETQ THA1 (ASSOC THAL (CDR THA1)))) (SETQ THA1 @(0Q 0Q))])
	(SETQ THRN (CADR THA1))
	(SETQ THA1 (CDDR THA1))
	(AND [EQ THWH @THASSERTION] [GO THP2])
	(COND [(NOT (SETQ THA2 (GET @THVRB THWH))) (SETQ THA2 @(0Q 0Q))]
	      [(NOT (SETQ THA2 (ASSOC THNF (CDR THA2)))) (SETQ THA2 @(0Q 0Q))]
	      [(NOT (SETQ THA2 (ASSOC THAL (CDR THA2)))) (SETQ THA2 @(0Q 0Q))])
	(SETQ THRVC (CADR THA2))
	(SETQ THA2 (CDDR THA2))
	(AND [GREATERP (PLUS THRVC THRN) THL] [GO THP1])
	(SETQ THL (PLUS THRVC THRN))
	(SETQ THL1 THA1)
	(SETQ THL2 THA2)
	(GO THP1)
   THP2 (COND [(EQ THRN 0Q) (RETURN NIL)]
	      [(GREATERP THL THRN) (SETQ THL1 THA1) (SETQ THL THRN)])
	(GO THP1)))
 EXPR)

(DEFPROP THMESSAGE
 (LAMBDA (THA)
  (THPUSH THTREE (CONS @THMESSAGE THA))
  THVALUE)
 FEXPR)

(DEFPROP THMESSAGE THPOPTV THSUCCEED)

(DEFPROP THMESSAGE THMESSAGEF THFAIL)

(DEFPROP THMESSAGEF
 (LAMBDA NIL
  (PROG (BOD)
	(SETQ BOD (CAR THTREE))
	(THPOPT)
	(COND [(AND [THBIND (CADR BOD)] [THMATCH1 (CADDR BOD) THMESSAGE])
	       (THPUSH THTREE (LIST @THPROG (CDDR BOD) NIL (CDDR BOD)))
	       (SETQ THMESSAGE NIL)
	       (RETURN (THPROGA))]
	      [T (SETQ THALIST THOLIST) (THPOPT)])
	(RETURN NIL)))
 EXPR)

(DEFPROP THMUNG THPOPTV THSUCCEED)

(DEFPROP THMUNG THMUNGF THFAIL)

(DEFPROP THMUNGF
 (LAMBDA NIL
  (EVLIS (CADAR THTREE))
  (THPOPT)
  NIL)
 EXPR)

(DEFPROP THNOFAIL
 (LAMBDA (THX)
  (COND [THX (DEFPROP THPROG THPROGT THFAIL)]
	[T (DEFPROP THPROG THPROGF THFAIL)]))
 EXPR)

(DEFPROP THNOHASH
 (LAMBDA (THA)
  (PROG (T1)
	(MAPC (FUNCTION (LAMBDA (X) (PUTPROP (CAR THA) @THNOHASH X)))
	      (SETQ T1 (OR [CDR THA] @[THASSERTION THCONSE THANTE THERASING])))
	(RETURN T1)))
 FEXPR)

(DEFPROP THNOT
 (LAMBDA (THA)
  (SETQ THEXP (LIST @THCOND (LIST (CAR THA) @(THFAIL THAND)) @((THSUCCEED)))))
 FEXPR)

(DEFPROP THNV (LAMBDA (X) (THV1 (CAR X))) FEXPR)

(DEFPROP THOR
 (LAMBDA (THA)
  (AND THA [THPUSH THTREE (LIST @THOR THA)] [SETQ THEXP (CAR THA)]))
 FEXPR)

(DEFPROP THOR THPOPTV THSUCCEED)

(DEFPROP THOR THORF THFAIL)

(DEFPROP THOR2
 (LAMBDA (P)
  (COND [THMESSAGE (THPOPT) NIL]
	[(AND [CADAR THTREE] [CDADAR THTREE])
	 (RPLACA (CDAR THTREE) (CDADAR THTREE))
	 (SETQ THEXP 
	       (COND [P (PROG1 (CAADAR THTREE) (OR [CADAR THTREE] [THPOPT]))]
		     [(CAR (CAADAR THTREE))]))]
	[T (THPOPT) NIL]))
 EXPR)

(DEFPROP THORF (LAMBDA NIL (THOR2 T)) EXPR)

(DEFPROP THPOPTV
 (LAMBDA NIL (SETQ THTREE (CDR THTREE)) THVALUE)
 EXPR)

(DEFPROP THPROG
 (LAMBDA (THA)
  (THBIND (CAR THA))
  (THPUSH THTREE (LIST @THPROG THA NIL THA))
  (THPROGA))
 FEXPR)

(DEFPROP THPROG THPROGT THSUCCEED)

(DEFPROP THPROG THPROGF THFAIL)

(DEFPROP THPROGA
 (LAMBDA NIL
  ((LAMBDA (X)
    (COND [(NULL (CDAR X)) (THPOPT) @THNOVAL]
	  [(ATOM (CADAR X))
	   (SETQ THEXP (LIST @THTAG (CADAR X)))
	   (RPLACA X (CDAR X))
	   THVALUE]
	  [T (SETQ THEXP (CADAR X)) (RPLACA X (CDAR X)) THVALUE]))
   (CDAR THTREE)))
 EXPR)

(DEFPROP THPROGF
 (LAMBDA NIL (THBRANCHUN) NIL)
 EXPR)

(DEFPROP THPROGT
 (LAMBDA NIL (THBRANCH) (THPROGA))
 EXPR)

(DEFPROP THPURE
 (LAMBDA (XX)
  (ERRSET (MAPC (FUNCTION (LAMBDA (Y) (AND [THVAR Y] [ERR NIL]))) XX)))
 EXPR)

(DEFPROP THPUTPROP
 (LAMBDA (ATO VAL IND)
  (THPUSH THTREE 
	  (LIST @THMUNG
		(LIST (LIST @PUTPROP
			    (LIST @QUOTE ATO)
			    (LIST @QUOTE (GET ATO IND))
			    (LIST @QUOTE IND)))))
  (PUTPROP ATO VAL IND))
 EXPR)

(DEFPROP THREM1
 (LAMBDA (THB)
  (PROG (THA THSV THA1 THA2 THA3 THA4 THA5 THONE THPC)
	(SETQ THNF (ADD1 THNF))
	(COND [(NUMBERP THB) (RETURN @THVRB)]
	      [(AND [ATOM THB] [NOT (EQ THB @?)]) (SETQ THA THB)]
	      [(OR [EQ THB @?] [MEMQ (CAR THB) @(THV THNV)])
	       (COND [THFST (RETURN @THVRB)] [(SETQ THA @THVRB)])]
	      [T (RETURN @THVRB)])
	(SETQ THA1 (GET THA THWH))
	(COND [THA1] [T (RETURN NIL)])
	(COND [(EQ THA1 @THNOHASH) (RETURN @THBQF)])
	(SETQ THA2 (THBA THNF THA1))
	(COND [THA2] [T (RETURN NIL)])
	(SETQ THA3 (THBA THAL (CADR THA2)))
	(COND [THA3] [T (RETURN NIL)])
	(SETQ THA4 (CADR THA3))
	(SETQ THPC (NOT (EQ THWH @THASSERTION)))
	(SETQ THA5 
	      (COND [(OR THFST THFSTP) (THBAP THBS (CDR THA4))]
		    [(THBA (COND [THPC THON] [T (CAR THON)]) (CDR THA4))]))
	(COND [THA5] [T (RETURN NIL)])
	(SETQ THONE (CADR THA5))
	(RPLACD THA5 (CDDR THA5))
	(COND [(AND [NOT (EQ (CADR THA4) 1Q)]
		    [OR [SETQ THSV (CDDR THA4)] T]
		    [RPLACA (CDR THA4) (SUB1 (CADR THA4))])
	       (RETURN THONE)])
	(SETQ THSV (CDDR THA3))
	(RPLACD THA3 THSV)
	(COND [(CDADR THA2)] [T (RETURN THONE)])
	(SETQ THSV (CDDR THA2))
	(RPLACD THA2 THSV)
	(COND [(CDR THA1)] [T (RETURN THONE)])
	(REMPROP THA THWH)
	(RETURN THONE)))
 EXPR)

(DEFPROP THREMBIND THREMBINDT THSUCCEED)

(DEFPROP THREMBIND THREMBINDF THFAIL)

(DEFPROP THREMBINDF
 (LAMBDA NIL
  (SETQ THALIST (CADAR THTREE))
  (THPOPT)
  NIL)
 EXPR)

(DEFPROP THREMBINDT
 (LAMBDA NIL
  (SETQ THALIST (CADAR THTREE))
  (THPOPT)
  THVALUE)
 EXPR)

(DEFPROP THREMOVE
 (LAMBDA (THB)
  (PROG (THB1 THWH THNF THAL THON THBS THFST THFSTP THFOO)
	(SETQ THNF 0Q)
	(SETQ THB1 
	      (COND [(ATOM THB)
		     (SETQ THBS THB)
		     (SETQ THWH (CAR (SETQ THB1 (GET THB @THEOREM))))
		     (CADDR THB1)]
		    [(SETQ THWH @THASSERTION) (SETQ THBS THB)]))
	(SETQ THAL (LENGTH THB1))
	(SETQ THFST T)
   THP1 (COND [(NULL THB1)
	       (SETQ THB1 THFOO)
	       (SETQ THNF 0Q)
	       (SETQ THFST (SETQ THFOO NIL))
	       (SETQ THFSTP T)
	       (GO THP1)]
	      [(NULL (SETQ THON (THREM1 (CAR THB1)))) (RETURN NIL)]
	      [(MEMQ THON @(THBQF THVRB))
	       (SETQ THFOO 
		     (NCONC THFOO (LIST (COND [(EQ THON @THVRB) (CAR THB1)]))))
	       (SETQ THB1 (CDR THB1))
	       (GO THP1)])
	(SETQ THFST NIL)
	(MAPC (FUNCTION THREM1) (CDR THB1))
	(SETQ THNF 0Q)
	(MAPC (FUNCTION THREM1) THFOO)
	(RETURN THON)))
 EXPR)

(DEFPROP THREMPROP
 (LAMBDA (ATO IND)
  (THPUSH THTREE 
	  (LIST @THMUNG
		(LIST (LIST @PUTPROP
			    (LIST @QUOTE ATO)
			    (LIST @QUOTE (GET ATO IND))
			    (LIST @QUOTE IND)))))
  (REMPROP ATO IND))
 EXPR)

(DEFPROP THRESTRICT
 (LAMBDA (THB)
  (PROG (X)
	(COND [(ATOM (SETQ X (THGAL (CAR THB) THALIST)))
	       (THPRINTC @THRESTRICT/ IGNORED/ -/ CONTINUING)]
	      [(THRPLACD (CDR X) (THUNION (CDDR X) (CDR THB)))])
	(RETURN X)))
 FEXPR)

(DEFPROP THRETURN
 (LAMBDA (X)
  (APPLY# @THSUCCEED (CONS @THPROG X)))
 FEXPR)

(DEFPROP THRPLACA
 (LAMBDA (X Y)
  (PROG (THML)
	(THRPLACAS X Y)
	(THPUSH THTREE (LIST @THMUNG THML))
	(RETURN X)))
 EXPR)

(DEFPROP THRPLACAS
 (LAMBDA (X Y)
  (THPUSH THML (LIST @THURPLACA X (CAR X)))
  (RPLACA X Y))
 EXPR)

(DEFPROP THURPLACA
 (LAMBDA (L) (RPLACA (CAR L) (CADR L)))
 FEXPR)

(DEFPROP THRPLACD
 (LAMBDA (X Y)
  (PROG (THML)
	(THRPLACDS X Y)
	(THPUSH THTREE (LIST @THMUNG THML))
	(RETURN X)))
 EXPR)

(DEFPROP THRPLACDS
 (LAMBDA (X Y)
  (THPUSH THML (LIST @THURPLACD X (CDR X)))
  (RPLACD X Y))
 EXPR)

(DEFPROP THURPLACD
 (LAMBDA (L) (RPLACD (CAR L) (CADR L)))
 FEXPR)

(DEFPROP THSETQ
 (LAMBDA (THL1)
  (PROG (THML THL)
	(SETQ THL THL1)
   LOOP (COND [(NULL THL) (THPUSH THTREE (LIST @THMUNG THML)) (RETURN THVALUE)]
	      [(NULL (CDR THL))
	       (PRINT THL1)
	       (THERT ODD NUMBER OF GOODIES - THSETQ)]
	      [(ATOM (CAR THL))
	       (THPUSH THML 
		       (LIST @SETQ (CAR THL) (LIST @QUOTE (EVAL (CAR THL)))))
	       (SET (CAR THL) (SETQ THVALUE (EVAL (CADR THL))))]
	      [T (THRPLACAS (CDR (THSGAL (CAR THL)))
			    (SETQ THVALUE (THVAL (CADR THL) THALIST)))])
	(SETQ THL (CDDR THL))
	(GO LOOP)))
 FEXPR)

(DEFPROP THSGAL
 (LAMBDA (X)
  (OR [ASSOC (CADR X) THALIST]
      [PROG (Y)
	    (SETQ Y (LIST (CADR X) @THUNASSIGNED))
	    (NCONC (GET @THALIST @VALUE) (LIST Y))
	    (RETURN Y)]))
 EXPR)

(DEFPROP THSTATE
 (LAMBDA (THINDICATORS)
  (PROG (THP THSLIST THGRIN)
	(MAPC
	 (FUNCTION
	  (LAMBDA (BUCKET)
	   (MAPC
	    (FUNCTION
	     (LAMBDA (THATOM)
	      (MAPC
	       (FUNCTION
		(LAMBDA (THWH)
		 (AND
		  [SETQ THP (GET THATOM THWH)]
		  [SETQ THP (ASSOC 1Q (CDR THP))]
		  [MAPC
		   (FUNCTION
		    (LAMBDA (LENGTH-BUCKET)
		     (MAPC (FUNCTION (LAMBDA (ASRT)
				      (COND [(EQ THWH @THASSERTION)
					     (SETQ THSLIST (CONS ASRT THSLIST))]
					    [T (SETQ THSLIST 
						     (CONS (NCONS ASRT) THSLIST)
						)
					       (SETQ THGRIN (CONS ASRT THGRIN))]
				       )))
			   (CDDR LENGTH-BUCKET))))
		   (CDR THP)])))
	       (COND [THINDICATORS] [@(THASSERTION THANTE THCONSE THERASING)])))
	     )
	    BUCKET)))
	 OBLIST)
	(EVAL (CONS @GRINDEF (DREVERSE THGRIN)))
	(COND [(OUTCH)
	       (PRINT (LIST @SETQ @THGENAME THGENAME))
	       (PRINT @(THDATA))])
	(MAPC (FUNCTION PRINT) THSLIST)
	(PRINT NIL)))
 FEXPR)

(DEFPROP THSUCCEED
 (LAMBDA (THA)
  (OR [NOT THA]
      [PROG (THX)
	    (SETQ THBRANCH THTREE)
	    (SETQ THABRANCH THALIST)
       LOOP (COND [(NULL THTREE) (PRINT THA) (THERT OVERPOP - THSUCCEED)]
		  [(EQ (CAAR THTREE) @THREMBIND)
		   (SETQ THALIST (CADAR THTREE))
		   (THPOPT)
		   (GO LOOP)]
		  [(EQ (CAAR THTREE) (CAR THA))
		   (THPOPT)
		   (RETURN (COND [(CDR THA) (EVAL (CADR THA))] [@THNOVAL]))]
		  [(AND [EQ (CAR THA) @THTAG]
			[EQ (CAAR THTREE) @THPROG]
			[SETQ THX (MEMQ (CADR THA) (CADDDR (CAR THTREE)))])
		   (RPLACA (CDAR THTREE) (CONS NIL THX))
		   (RETURN (THPROGT))]
		  [T (THPOPT) (GO LOOP)])]))
 FEXPR)

(DEFPROP THTAE
 (LAMBDA (XX)
  (COND [(ATOM XX) NIL]
	[(EQ (CAR XX) @THUSE)
	 (MAPCAR (FUNCTION (LAMBDA (X)
			    (COND [(NOT (AND [SETQ THXX (GET X @THEOREM)]
					     [EQ (CAR THXX) TYPE]))
				   (PRINT X)
				   (LIST @THAPPLY
					 (THERT BAD THEOREM -THTAE)
					 (CAR THX))]
				  [T (LIST @THAPPLY X (CAR THX))])))
		 (CDR XX))]
	[(EQ (CAR XX) @THTBF)
	 (MAPCAN (FUNCTION (LAMBDA (Y)
			    (COND [((CADR XX) Y)
				   (LIST (LIST @THAPPLY Y (CAR THX)))])))
		 (COND [THY1 THY]
		       [(SETQ THY1 T) (SETQ THY (THMATCHLIST (CAR THX) TYPE))]))
	 ]
	[T (PRINT XX) (THTAE (THERT UNCLEAR RECCOMMENDATION -THTAE))]))
 EXPR)

(DEFPROP THTAG
 (LAMBDA (L)
  (AND [CAR L] [THPUSH THTREE (LIST @THTAG (CAR L))]))
 FEXPR)

(DEFPROP THTAG THPOPTV THSUCCEED)

(DEFPROP THTAG THTAGF THFAIL)

(DEFPROP THTAGF (LAMBDA NIL (THPOPT) NIL) EXPR)

(DEFPROP THTRUE (LAMBDA (X) T) EXPR)

(DEFPROP THTRY1
 (LAMBDA NIL
  (PROG (THX THY THZ THW THEOREM)
	(SETQ THZ (CAR THTREE))
	(SETQ THY (CDDR THZ))
	(RPLACD THY (SUB1 (CDR THY)))
 NXTREC (COND [(OR [NULL (CAR THY)] [ZEROP (CDR THY)]) (RETURN NIL)])
	(SETQ THX (CAAR THY))
	(GO (CAR THX))
  THNUM (RPLACD THY (CADR THX))
	(RPLACA THY (CDAR THY))
	(GO NXTREC)
  THDBF (SETQ THOLIST THALIST)
	(COND [(NULL (CADDR THX)) (RPLACA THY (CDAR THY)) (GO NXTREC)]
	      [(PROG (XVAL)
		     (SETQ XVAL 
			   (AND [(CADR THX) (SETQ THW (CAADDR THX))]
				[THMATCH1 (CADR THZ) (CAR THW)]))
		     (RPLACA (CDDR THX) (CDADDR THX))
		     (RETURN XVAL))
	       (RETURN THW)]
	      [T (GO THDBF)])
  THTBF (COND [(NULL (CADDR THX)) (RPLACA THY (CDAR THY)) (GO NXTREC)])
	(SETQ THEOREM (CAADDR THX))
 THTBF1 (COND [(NOT (AND [SETQ THW (GET THEOREM @THEOREM)]
			 [EQ (CAR THW) @THCONSE]))
	       (PRINT THEOREM)
	       (COND [(EQ (SETQ THEOREM (THERT BAD THEOREM - THTRY1)) @T)
		      (GO NXTREC)]
		     [T (GO THTBF1)])])
	(COND [(PROG (XVAL)
		     (SETQ XVAL 
			   (AND [(CADR THX) (CAADDR THX)]
				[THAPPLY1 THEOREM THW (CADR THZ)]))
		     (RPLACA (CDDR THX) (CDADDR THX))
		     (RETURN XVAL))
	       (RETURN T)]
	      [T (GO THTBF)])))
 EXPR)

(DEFPROP THTRY
 (LAMBDA (X)
  (COND [(ATOM X) NIL]
	[(EQ (CAR X) @THTBF)
	 (COND [(NOT THZ1) (SETQ THZ1 T) (SETQ THZ (THMATCHLIST THA2 @THCONSE))]
	  )
	 (COND [THZ (LIST (LIST @THTBF (CADR X) THZ))] [T NIL])]
	[(EQ (CAR X) @THDBF)
	 (COND [(NOT THY1)
		(SETQ THY1 T)
		(SETQ THY (THMATCHLIST THA2 @THASSERTION))])
	 (COND [THY (LIST (LIST @THDBF (CADR X) THY))] [T NIL])]
	[(EQ (CAR X) @THUSE) (LIST (LIST @THTBF @THTRUE (CDR X)))]
	[(EQ (CAR X) @THNUM) (LIST X)]
	[T (PRINT X) (THTRY (THERT UNCLEAR RECOMMENDATION - THTRY))]))
 EXPR)

(DEFPROP THUNDO THUNDOT THSUCCEED)

(DEFPROP THUNDO THUNDOF THFAIL)

(DEFPROP THUNDOF
 (LAMBDA NIL
  (COND [(NULL (CADDAR THTREE)) (THPOPT)]
	[T (SETQ THXX (CDDAR THTREE))
	   (SETQ THALIST (CAADR THXX))
	   (RPLACA (CDR THXX) (CDADR THXX))
	   (SETQ THTREE (CAAR THXX))
	   (RPLACA THXX (CDAR THXX))])
  NIL)
 EXPR)

(DEFPROP THUNDOT (LAMBDA NIL (THPOPT) T) EXPR)

(DEFPROP THUNIQUE
 (LAMBDA (THA)
  (SETQ THA (CONS @THUNIQUE (MAPCAR (FUNCTION THUCI) THA)))
  (PROG (X)
	(SETQ X THALIST)
     LP (COND [(NULL X) (THPUSH THALIST THA) (RETURN T)]
	      [(EQ (CAAR X) @THUNIQUE)
	       (COND [(EQUAL (CAR X) THA) (RETURN NIL)])])
	(SETQ X (CDR X))
	(GO LP)))
 FEXPR)

(DEFPROP THUCI
 (LAMBDA (A)
  (COND [(MEMQ (CAR A) @(THV THNV))
	 (COND [(ATOM (SETQ A (THGAL A THALIST)))] [(CADR A)])]
	[(EVAL A)]))
 EXPR)

(DEFPROP THV1
 (LAMBDA (X)
  (SETQ THXX X)
  (COND [(EQ (SETQ X 
		   (CADR (OR [ASSOC X THALIST]
			     [PROG2 (PRINT THXX) (THERT THUNBOUND - THV1)])))
	     @THUNASSIGNED)
	 (PRINT THXX)
	 (THERT THUNASSIGNED - THV1)]
	[T X]))
 EXPR)

(DEFPROP THV (LAMBDA (X) (THV1 (CAR X))) FEXPR)

(DEFV THV (THV THNV))

(DEFPROP THVAL
 (LAMBDA (THEXP THALIST)
  (THPUSH THLEVEL (LIST THTREE THALIST))
  (PROG (THTREE THVALUE THBRANCH THOLIST THABRANCH THE THMESSAGE)
	(SETQ THV @(THV THNV))
	(SETQ THVALUE @THNOVAL)
     GO (SETQ THE THEXP)
	(SETQ THEXP NIL)
	(COND [↑A (SETQ ↑A NIL) (COND [(THERT ↑A - THVAL)] [T (GO FAIL)])])
	(COND [(ATOM (ERRSET (SETQ THVALUE (EVAL THE))))
	       (SETQ THLEVEL (CDR THLEVEL))
	       (ERR NIL)])
    GO1 (COND [THMESSAGE (GO MFAIL)]
	      [THEXP (GO GO)]
	      [THVALUE (GO SUCCEED)]
	      [T (GO FAIL)])
 SUCCEED 
	(COND [(NULL THBRANCH) (SETQ THBRANCH THTREE) (SETQ THABRANCH THALIST)])
	(COND [(NULL THTREE) (SETQ THLEVEL (CDR THLEVEL)) (RETURN THVALUE)]
	      [(SETQ THEXP (GET (CAAR THTREE) @THSUCCEED)) (GO GO2)]
	      [(THERT BAD SUCCEED - THVAL) (GO SUCCEED)]
	      [T (GO FAIL)])
  MFAIL (COND [(EQ (CAR THMESSAGE) THTREE)
	       (SETQ THEXP (CADR THMESSAGE))
	       (SETQ THMESSAGE NIL)
	       (GO GO)])
   FAIL (COND [(NULL THTREE) (SETQ THLEVEL (CDR THLEVEL)) (RETURN NIL)]
	      [(SETQ THEXP (GET (CAAR THTREE) @THFAIL)) (GO GO2)]
	      [(THERT BAD FAIL - THVAL) (GO SUCCEED)]
	      [T (GO FAIL)])
    GO2 (SETQ THVALUE ((PROG1 THEXP (SETQ THEXP NIL))))
	(GO GO1)))
 EXPR)

(DEFPROP THVAR
 (LAMBDA (X)
  (COND [(ATOM X) NIL] [T (MEMQ (CAR X) @(THV THNV))]))
 EXPR)

(DEFPROP THVARS2
 (LAMBDA (X)
  (PROG (A)
	(COND [(ATOM X) (RETURN X)])
	(AND [EQ (CAR X) @THEV] [SETQ X (THVAL (CADR X) THALIST)])
	(COND [(THVAR X)] [T (RETURN X)])
	(SETQ A (THGAL X THALIST))
	(RETURN (COND [(EQ (CADR A) @THUNASSIGNED) X]
		      [(AND THY [EQ (CAR X) @THNV])
		       (THRPLACA (CDR A) @THUNASSIGNED)
		       X]
		      [T (CADR A)]))))
 EXPR)

(DEFPROP THVARSUBST
 (LAMBDA (THX THY)
  (COND [(EQ (CAR THX) @THEV) (SETQ THX (THVAL (CADR THX) THALIST))]
	[(THVAR THX) (SETQ THX (EVAL THX))])
  (COND [(ATOM THX) THX] [T (MAPCAR (FUNCTION THVARS2) THX)]))
 EXPR)

(DEFPROP THVSETQ
 (LAMBDA (THA)
  (PROG (A)
	(SETQ A THA)
   LOOP (COND [(NULL A) (RETURN THVALUE)]
	      [(NULL (CDR A)) (PRINT THA) (THERT ODD NUMBER OF GOODIES-THSETQ)]
	      [T (SETQ THVALUE 
		       (CAR (RPLACA (CDR (THSGAL (CAR A)))
				    (THVAL (CADR A) THALIST))))])
	(SETQ A (CDDR A))
	(GO LOOP)))
 FEXPR)

(DEFPROP THREAD
 (LAMBDA NIL
  (PROG (CHAR X)
	(RETURN (SELECTQ [SETQ CHAR (READCH)]
			 [? (LIST @THV (READ))]
			 [: (LIST @THV (READ))]
			 [E (LIST @THEV (READ))]
			 [← (LIST @THNV (READ))]
			 [& (PROG NIL
			     CHLP (COND [(NEQ @& (READCH)) (GO CHLP)]))]
			 [T @(THTBF THTRUE)]
			 [R @THRESTRICT]
			 [G @THGOAL]
			 [A @THASSERT]
			 [P @$P]
			 [N (LIST @THANUM (READ))]
			 [COND [(SETQ X (ASSOC CHAR THUSERCHARS))
				(EVAL (CONS @PROGN (CDR X)))]
			       [(PRINT @ILLEGAL-PREFIX)
				(PRINC @$)
				(PRINC CHAR)
				(PRINC (READ))
				(ERR NIL)]]))))
 EXPR)

(DEFV THUSERCHARS NIL)

(DEFPROP THERT
 (LAMBDA (/0ERTA)
  (PROG (/0LISTEN ↑W ↑Q /0RETVAL /0RETFLAG)
	(SETQ ↑Q (INC NIL NIL))
	(SETQ ↑W (OUTC NIL NIL))
	(SETQ /0LEVEL (ADD1 /0LEVEL))
	(PRINT @>>>)
	(COND [(EQ (CAR /0ERTA) @TH%0%)
	       (MAPC (FUNCTION THPRINT2) (CDR /0ERTA))
	       (INC ↑Q (SETQ ↑Q NIL))]
	      [/0ERTA (MAPC (FUNCTION THPRINT2) /0ERTA)
		      (PRINT @LISTENING)
		      (OR THLEVEL [THPRINT2 @THVAL])])
	(SETQ /0RETVAL T)
 /0LISTEN 
	(SETQ THINF NIL)
	(SETQ /0RETFLAG NIL)
	(TERPRI)
	(TERPRI)
	(AND [NEQ (CAR /0ERTA) @TH%0%]
	     [PROG (BASE *NOPOINT)
		   (SETQ BASE 12Q)
		   (SETQ *NOPOINT T)
		   (PRINC /0LEVEL)])
	(ERRSET (COND [(EQ (SETQ /0LISTEN (READ)) @$P) (SETQ /0RETFLAG T)]
		      [(AND [NOT (ATOM /0LISTEN)] [EQ (CAR /0LISTEN) @$P])
		       (SETQ /0RETVAL (EVAL (CADR /0LISTEN)))
		       (SETQ /0RETFLAG T)]
		      [THLEVEL (PRINT (EVAL /0LISTEN))]
		      [T (PRINT (THVAL /0LISTEN THALIST))]))
	(AND [NULL /0RETFLAG] [GO /0LISTEN])
	(SETQ /0LEVEL (SUB1 /0LEVEL))
	(INC ↑Q NIL)
	(OUTC ↑W NIL)
	(RETURN /0RETVAL)))
 FEXPR)

(DEFPROP THINIT
 (LAMBDA NIL
  (SETQ THINF (SETQ THTREE (SETQ THLEVEL NIL)))
  (SETQ /0LEVEL -1Q)
  (COND [THUSERMESSAGES
	 (MAPC (FUNCTION (LAMBDA (X) (TERPRI) (PRINC X))) THUSERMESSAGES)
	 (SETQ THUSERMESSAGES NIL)
	 (AND [ERRSET (INC (INPUT DSK: (INIT . PLN)) NIL) NIL]
	      [THERT TH%0% READING (INIT . PLN)])])
  (AND THUSERINITFN [THUSERINITFN])
  (TERPRI)
  (SETQ %%TIME (TIME))
  (SETQ %%DTIME (DTIME))
  (SETQ %%GCTIME (GCTIME))
  (SETQ %%SPEAK (SPEAK))
  (THERT TOP LEVEL))
 EXPR)

(DEFPROP THINITFN
 (LAMBDA (X)
  (PROG1 THUSERINITFN (SETQ THUSERINITFN X)))
 EXPR)

(DEFPROP THEDIT
 (LAMBDA (X)
  (PROG (Y)
	(COND [(NULL X) (SETQ X (NCONS LASTWORD))])
	(COND [(SETQ Y (GET (CAR X) @THEOREM))
	       (EDITE Y (CDR X) (CAR X))
	       (RETURN (SETQ LASTWORD (CAR X)))]
	      [T (PRINT (CAR X)) (PRINC @"not editable.") (ERR NIL)])))
 FEXPR)

(DEFPROP THTRACE
 (LAMBDA (L) (MAPC (FUNCTION THTRACE1) L) L)
 FEXPR)

(DEFV THTRACE NIL)

(DEFPROP THTRACE1
 (LAMBDA (X)
  (PROG (Y)
	(SETQ X 
	      (COND [(ATOM X) (LIST X T NIL)]
		    [(CDDR X) X]
		    [(NULL (CDR X)) (PRINT X) (PRINC @BAD/ FORMAT) (RETURN NIL)]
		    [(LIST (CAR X) (CADR X) NIL)]))
	(COND [(GET (CAR X) @THEOREM)
	       (COND [(SETQ Y (ASSOC @THEOREM THTRACE))
		      (RPLACD Y @((THSEL @CADR) (THSEL @CADDR)))]
		     [(SETQ THTRACE 
			    (LIST X 
				  (APPEND @(THEOREM (THSEL @CADR)
						    (THSEL @CADDR))
					  THTRACE)))])])
	(COND [(SETQ Y (ASSOC (CAR X) THTRACE)) (RPLACD Y (CDR X))]
	      [(SETQ THTRACE (CONS X THTRACE))])
	(RETURN X)))
 EXPR)

(DEFPROP THUNTRACE
 (LAMBDA (L)
  (COND [L (SETQ THTRACE 
		 (MAPCAN (FUNCTION (LAMBDA (X)
				    (COND [(MEMQ (CAR X) L) (PRINT X) NIL]
					  [(LIST X)])))
			 THTRACE))]
	[THTRACE (MAPC (FUNCTION PRINT) THTRACE) (SETQ THTRACE NIL)])
  @DONE)
 FEXPR)

(DEFPROP THTRACES
 (LAMBDA (THF THL)
  (PROG (THY THZ THB)
	(AND [SETQ THY (ASSOC THF THTRACE)]
	     [OR [SETQ THB (THVAL (CADDR THY) THALIST)]
		 [THVAL (CADR THY) THALIST]]
	     [OR [SETQ THZ (GET THF @THTRACE)] [THERT THTRACES - TRACE LOSSAG]]
	     [THZ THL THB]
	     THB 
	     [THERT])))
 EXPR)

(DEFPROP THTRACES
 (LAMBDA NIL
  (PRINT (CADAR THTREE))
  (PRINC @SUCCEEDED/ )
  (EVLIS (CDDAR THTREE))
  (THPOPT)
  THVALUE)
 THSUCCEED)

(DEFPROP THTRACES
 (LAMBDA NIL
  (PRINT (CADAR THTREE))
  (PRINC @FAILED/ )
  (EVLIS (CDDAR THTREE))
  (THPOPT)
  NIL)
 THFAIL)

(DEFPROP THSEL
 (LAMBDA (THF)
  (PROG (THX)
	(RETURN (AND [SETQ THX (ASSOC THL THTRACE)]
		     [SETQ THX (THF THX)]
		     [THVAL THX THALIST]))))
 EXPR)

(DEFPROP THGENS
 (LAMBDA (X)
  (PROG (BASE *NOPOINT)
	(SETQ BASE 12Q)
	(SETQ *NOPOINT T)
	(RETURN (MAKNAM (NCONC (EXPLODE (CAR X))
			       (EXPLODE (SETQ THGENS (ADD1 THGENS))))))))
 FEXPR)

(DEFV THGENS 0Q)

(DEFPROP THPP-THCONSE
 (LAMBDA (L)
  (PP-FORMAT L (COND [(MEMB @THNOASSERT L) 3Q] [T 2Q]) @LABELS))
 EXPR)

(DEFPROP THPP-THFIND
 (LAMBDA (L) (PP-FORMAT L 3Q @LABELS))
 EXPR)

(DEFPROP THPP-THMESSAGE
 (LAMBDA (L) (PP-FORMAT L 2Q @LABELS))
 EXPR)

(NCONC PRETTYPROPS @(THEOREM THSUCCEED THFAIL THTRACE))

(DEFV THUSERINITFN NIL)

(DEFV ↑A NIL)

(DEFV THXX NIL)

(DEFV THALIST ((NIL NIL)))

(DEFV THUSERMESSAGES (MICRO-PLANNER))

(PROGN
(DEFPROP PINIT
 (LAMBDA NIL
  (MODCHR (CHRVAL @') (MODCHR (CHRVAL @/@) NIL))
  (DRM $ THREAD)
  (DRM : THREAD)
  (DEFPROP THV "$?" PRINTMACRO)
  (DEFPROP THNV "$←" PRINTMACRO)
  (DEFPROP THANUM "$N" PRINTMACRO)
  (DEFPROP THCONSE THPP-THCONSE PRINTMACRO)
  (DEFPROP THANTE THPP-THCONSE PRINTMACRO)
  (DEFPROP THERASING THPP-THCONSE PRINTMACRO)
  (DEFPROP THFIND THPP-THFIND PRINTMACRO)
  (DEFPROP THMESSAGE THPP-THMESSAGE PRINTMACRO)
  (DEFPROP THPROG PP-LABELS PRINTMACRO)
  (DEFPROP THCOND BRACKETS PRINTMACRO)
  (DEFPROP THOR BRACKETS PRINTMACRO)
  (DEFPROP THAND BRACKETS PRINTMACRO)
  (DEFPROP THDO BRACKETS PRINTMACRO)
  (INITFN @THINIT)
  T)
 EXPR)

(DEFPROP PUNINIT
 (LAMBDA NIL
  (MAPC (FUNCTION (LAMBDA (X) (REMPROP X @PRINTMACRO)))
	@(THV THNV THANUM THCONSE THANTE THERASING THFIND THMESSAGE THPROG
	      THCOND THOR THAND THDO))
  (MODCHR (CHRVAL @') (MODCHR 43Q NIL))
  (MODCHR (CHRVAL @$) (MODCHR 43Q NIL))
  (MODCHR (CHRVAL @:) (MODCHR 43Q NIL))
  (SETQ THXX NIL)
  (SETQ THALIST (LIST (LIST NIL NIL)))
  (SETQ THUSERMESSAGES @(MICRO-PLANNER))
  (SETQ THGENS 0Q)
  (SETQ THGENAME 0Q)
  (INITFN NIL)
  T)
 EXPR)

(DEFPROP PCLEANUP
 (LAMBDA NIL
  (REMOB PLNRFNS PINIT PUNINIT PCLEANUP)
  (RPLACD (MEMQ @THEOREM GRINPROPS) NIL)
  (THFLUSH)
  (EXCISE)
  (GC)
  T)
 EXPR)
)

(NOCOMPILE
(DEFV PLNRFNS ((DECLARE (*FEXPR THAPPLY THGENAME THSTATE THANTE THERASING 
	       THCONSE THDUMP THRESTRICT THBKPT THUNIQUE) (*FEXPR THVSETQ 
	       THMESSAGE THDO THGOAL THERASE THAND THNV THSUCCEED THAMONG 
	       THCOND THSETQ) (*FEXPR THASSERT THASVAL THERT THGO THFAIL THOR 
	       THFIND THFINALIZE THRETURN THPROG THFLUSH) (*FEXPR THNOT THV 
	       THTRACE THGENS) (*LSUBR THMATCH) (SPECIAL THLAS OBLIST THINF 
	       THGENAME THGENS THZ THY THX THALIST THABRANCH THBRANCH) 
	       (SPECIAL THV /0RETVAL /0LISTEN THL /0RETFLAG THE /0LEVEL THXX 
	       THTT TYPE THWH THON THML) (SPECIAL THBS THNF THPC XX THAL THZ1 
	       THY1 ↑A THTTL THA2 LASTWORD THFSTP THFST) (SPECIAL THUSERCHARS 
	       THEXP THTREE THLEVEL THTRACE THPRD THMESSAGE THUSERMESSAGES) 
	       (SPECIAL THUNREADFLG THUNREAD1 THUNREAD2 THOLIST THVALUE 
	       THUSERINITFN) (SPECIAL BASE *NOPOINT %%TIME %%DTIME %%GCTIME %%SPEAK) 
	       (DE THCMPDEF (X) (COND ((ATOM (CADDR X)) (FLUSHEXPR X)) 
	       (T (COMPFUNC (CADR X) (CONS (QUOTE SUBR) (CDADDR X)) (CADDDR X)))
	       )) (DEFLIST (THFAIL THSUCCEED THTRACE) THCMPDEF DEFACTION)) 
	       THPUSH THPOPT EVLIS THPRINT2 THPRINTC THADD THAMONG THAMONGF 
	       THAND THANDF THANDT THANTE THAPPLY THAPPLY1 THEOREM THASS1 
	       THASSERT THASSERTF THASSERTT THASVAL THBA THBAP THBIND THBI1 
	       THBKPT THBRANCH THBRANCHUN THCOND THCONDF THCONDT THCONSE 
	       THDATA THDEF THDO THDO1 THDOB THDUMP THERASE THERASEF THERASET 
	       THERASING THFAIL THFAIL? THFAIL?F THFINALIZE THFIND THFINDF 
	       THFINDT THFLUSH THGAL THGENAME THGO THGOAL THGOALF THGOALT 
	       THIP THMATCH2 THCHECK THUNION THMATCH THMATCH1 THMATCHLIST 
	       THMESSAGE THMESSAGEF THMUNG THMUNGF THNOFAIL THNOHASH THNOT 
	       THNV THOR THOR2 THORF THPOPTV THPROG THPROGA THPROGF THPROGT 
	       THPURE THPUTPROP THREM1 THREMBIND THREMBINDF THREMBINDT 
	       THREMOVE THREMPROP THRESTRICT THRETURN THRPLACA THRPLACAS 
	       THURPLACA THRPLACD THRPLACDS THURPLACD THSETQ THSGAL THSTATE 
	       THSUCCEED THTAE THTAG THTAGF THTRUE THTRY1 THTRY THUNDO 
	       THUNDOF THUNDOT THUNIQUE THUCI THV1 THV THVAL THVAR THVARS2 
	       THVARSUBST THVSETQ (*PG*) THREAD THUSERCHARS THERT THINIT 
	       THINITFN THEDIT THTRACE THTRACE1 THUNTRACE THTRACES THSEL 
	       THGENS THPP-THCONSE THPP-THFIND THPP-THMESSAGE (NCONC 
	       PRETTYPROPS (QUOTE (THEOREM THSUCCEED THFAIL THTRACE))) 
	       THUSERINITFN ↑A THXX THALIST THUSERMESSAGES (MBD: PROGN PINIT 
	       PUNINIT PCLEANUP)))
)